Search Results

Documents authored by Ehrhard, Thomas

Document
DOI: 10.4230/LIPIcs.FSCD.2023.8
The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

Authors: Thomas Ehrhard, Claudia Faggian, and Michele Pagani

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.
Cite as

Thomas Ehrhard, Claudia Faggian, and Michele Pagani. The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ehrhard_et_al:LIPIcs.FSCD.2023.8,
  author =	{Ehrhard, Thomas and Faggian, Claudia and Pagani, Michele},
  title =	{{The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.8},
  URN =		{urn:nbn:de:0030-drops-179926},
  doi =		{10.4230/LIPIcs.FSCD.2023.8},
  annote =	{Keywords: Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.17
Differentials and Distances in Probabilistic Coherence Spaces

Authors: Thomas Ehrhard

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.
Cite as

Thomas Ehrhard. Differentials and Distances in Probabilistic Coherence Spaces. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ehrhard:LIPIcs.FSCD.2019.17,
  author =	{Ehrhard, Thomas},
  title =	{{Differentials and Distances in Probabilistic Coherence Spaces}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.17},
  URN =		{urn:nbn:de:0030-drops-105243},
  doi =		{10.4230/LIPIcs.FSCD.2019.17},
  annote =	{Keywords: Denotational semantics, probabilistic coherence spaces, differentials of programs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.259
Collapsing non-idempotent intersection types

Authors: Thomas Ehrhard

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We proved recently that the extensional collapse of the relational model of linear logic coincides with its Scott model, whose objects are preorders and morphisms are downwards closed relations. This result is obtained by the construction of a new model whose objects can be understood as preorders equipped with a realizability predicate. We present this model, which features a new duality, and explain how to use it for reducing normalization results in idempotent intersection types (usually proved by reducibility) to purely combinatorial methods. We illustrate this approach in the case of the call-by-value lambda-calculus, for which we introduce a new resource calculus, but it can be applied in the same way to many different calculi.
Cite as

Thomas Ehrhard. Collapsing non-idempotent intersection types. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 259-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{ehrhard:LIPIcs.CSL.2012.259,
  author =	{Ehrhard, Thomas},
  title =	{{Collapsing non-idempotent intersection types}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{259--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.259},
  URN =		{urn:nbn:de:0030-drops-36776},
  doi =		{10.4230/LIPIcs.CSL.2012.259},
  annote =	{Keywords: Linear logic, lambda-calculus, denotational semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.1
Resource Lambda-Calculus: the Differential Viewpoint

Authors: Thomas Ehrhard

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We present differential linear logic and its models, the associated resource and differential lambda-calculi, and the Taylor expansion of promotion boxes. We also describe an antiderivative which seems to be available in many models of differential Linear Logic, and we present a very simple categorical axiom for this operation.
Cite as

Thomas Ehrhard. Resource Lambda-Calculus: the Differential Viewpoint. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{ehrhard:LIPIcs.CSL.2011.1,
  author =	{Ehrhard, Thomas},
  title =	{{Resource Lambda-Calculus: the Differential Viewpoint}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{1--1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.1},
  URN =		{urn:nbn:de:0030-drops-32152},
  doi =		{10.4230/LIPIcs.CSL.2011.1},
  annote =	{Keywords: proof theory, lambda-calculus, linear logic, denotational semantics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.97
Full Abstraction for Resource Calculus with Tests

Authors: Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We study the semantics of a resource sensitive extension of the lambda-calculus in a canonical reflexive object of a category of sets and relations, a relational version of the original Scott D infinity model of the pure lambda-calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda-calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a ``must'' parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda-calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula.
Cite as

Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full Abstraction for Resource Calculus with Tests. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 97-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bucciarelli_et_al:LIPIcs.CSL.2011.97,
  author =	{Bucciarelli, Antonio and Carraro, Alberto and Ehrhard, Thomas and Manzonetto, Giulio},
  title =	{{Full Abstraction for Resource Calculus with Tests}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{97--111},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.97},
  URN =		{urn:nbn:de:0030-drops-32250},
  doi =		{10.4230/LIPIcs.CSL.2011.97},
  annote =	{Keywords: resource lambda calculus, relational semantics, full abstraction, differential linear logic}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact